Section: New Results

A simulation infrastructure for CCSL, the timing model of UML MARTE

Participants : Huafeng Yu, Loïc Besnard, Thierry Gautier, Jean-Pierre Talpin, Paul Le Guernic.

Clock Constraint Specification Language (CCSL) [32] is defined in an annex of the UML MARTE profile [48] . We are interested in the analysis, synthesis and code generation of multi-clocked/polychronous systems specified in CCSL. Timed systems subject to clock expressions or relations can be modeled, specified, analyzed, and simulated within the software environments, such as SCADE [41] , TimeSquare [44] and Polychrony. However, code generation from a multi-clocked system is far from obvious. For instance, SCADE always uses a reference or master clock (the fastest); all clocks and all conditions are defined as a functional sampling of this master clock, from the highest specification down to the lowest generated code. In TimeSquare, clock constraints are solved using a heuristic algorithm, which is generally non-deterministic. On the contrary, in Polychrony, a formally defined refinement process yields to the generation of (sequential or concurrent) code by the addition of control variables to get a deterministic behavior satisfying the constraints and allowing the desired amount of concurrency.

The motivation of our work, to address the simulation and code generation of polychronous systems, is to take advantage of the formal framework of Polychrony in the context of a high-level specification formalism, MARTE CCSL[22] . Yet, our work considers a novel approach with regards to previous approaches: to generate executable specifications by considering discrete controller synthesis (DCS) [50] , [45] , [46] . Clock constraint resolution is addressed by DCS, which does not necessarily require a master clock to address polychronous clocks. In our approach, polychronous (CCSL) specifications are first partitioned: clock relations are considered as control objectives, other constraints are considered as the system to be controlled. The all the constraints are translated into, via SIGNAL, polynomial dynamical systems (PDSs). A PDS represents the transition system of a specification as well as the constraints (invariants) it must satisfy. The Sigali tool is then used to generate the controller. Finally, the generated controller, together with the original system, is composed to complete the code generation for simulation. In our approach, the temporal semantics of CCSL is mapped onto a polychronous model of computation, on which effective synthesis is carried out to meet constraint requirements. This approach provides both a useful mapping in theory and a flow, which is practical in the generation of reactive controllers.